FDL - WFND_FUNCTIONALITY

WFND_FUNCTIONALITY_tcom

Functionality lemmas for wellfounded predicate.
NB: wellfounded_functionality_wrt_implies_a assumes
subtype abstraction is proper predicate. ie. has wf thm.

origin